$LOAD_PATH.unshift File.join(File.dirname(__FILE__),'..','ext_pr1/lib')
require 'ext_pr1_v4'

#volume of a hollow cube
#hollow_cube_volume::= (length_outer, length_inner, n)::
# Nat x Nat -> Nat where (length_outer >= length_inner)
# n == Nat
#Test{(3,2,1)=>19, (2,2,3)=>0, (0,0,3)=>0
#(-10)=>Err,(-10,4,4)=>Err,(4,"3",4)=>Err,(4,5,4)=>Err,(5,4,-1)=>Err}

def h_cube_volume(seitenlaenge_aussen, seitenlaenge_innen, n)
  check_pre((
  seitenlaenge_aussen.nat? and
  seitenlaenge_innen.nat? and
  n.nat? and
  (seitenlaenge_aussen >= seitenlaenge_innen)))
  wuerfel(seitenlaenge_aussen,n) - wuerfel(seitenlaenge_innen,n)
end
def wuerfel(seitenlaenge, n)
  seitenlaenge ** n
end

